ds:x:Id fp Type, da:k:Knd fp Type, x:ecl(ds;da), L:event-info(ds;da) List.
ecl-halt(ds;da;x)(0,L)  2of(2of(last(L)))  ecl-halt-type(da;x) 

latex

Definitions

b, t  T, P  Q, x:A. B(x), Void, x:A. B(x), Top, event-info(ds;da), last(L), 2of(t), Valtype(da;k), left+right, Unit, Type, Knd, ecl-halt-kind(x), x:AB(x), s = t, Id, x. t(x), a:A fp B(a), ecl(ds;da), type List, #$n, AB, a<b, False, A, {x:A| B(x) }, , , ecl-halt(ds;da;x), f(a), Case b of inl(x)  s(x) ; inr(y)  t(y), ecl-halt-type(da;x), True, {T}, SQType(T), Prop, s ~ t, inl(x), inr(x), true, false, x:AB(x), P & Q, P  Q, f(x)?z

Lemmas

subtype rel self, ma-valtype wf, false wf, ecl-halt-nil, last wf, bfalse wf, btrue wf, assert wf, Knd sq, ecl-halt wf, le wf, event-info wf, ecl wf, fpf wf, Id wf, ecl-halt-kind wf, Knd wf, unit wf, ecl-halt-kind-last